YES 20.981 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ CR

mainModule List
  ((insert :: Ratio Int  ->  [Ratio Int ->  [Ratio Int]) :: Ratio Int  ->  [Ratio Int ->  [Ratio Int])

module List where
  import qualified Maybe
import qualified Prelude

  insert :: Ord a => a  ->  [a ->  [a]
insert e ls insertBy compare e ls

  insertBy :: (a  ->  a  ->  Ordering ->  a  ->  [a ->  [a]
insertBy x [] x : []
insertBy cmp x ys@(y : ys'
case cmp x y of
  GT-> y : insertBy cmp x ys'
  _-> x : ys


module Maybe where
  import qualified List
import qualified Prelude



Case Reductions:
The following Case expression
case cmp x y of
 GT → y : insertBy cmp x ys'
 _ → x : ys

is transformed to
insertBy0 y cmp x ys' ys GT = y : insertBy cmp x ys'
insertBy0 y cmp x ys' ys _ = x : ys



↳ HASKELL
  ↳ CR
HASKELL
      ↳ BR

mainModule List
  ((insert :: Ratio Int  ->  [Ratio Int ->  [Ratio Int]) :: Ratio Int  ->  [Ratio Int ->  [Ratio Int])

module List where
  import qualified Maybe
import qualified Prelude

  insert :: Ord a => a  ->  [a ->  [a]
insert e ls insertBy compare e ls

  insertBy :: (a  ->  a  ->  Ordering ->  a  ->  [a ->  [a]
insertBy x [] x : []
insertBy cmp x ys@(y : ys'insertBy0 y cmp x ys' ys (cmp x y)

  
insertBy0 y cmp x ys' ys GT y : insertBy cmp x ys'
insertBy0 y cmp x ys' ys _ x : ys


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
ys@(vy : vz)

is replaced by the following term
vy : vz



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule List
  ((insert :: Ratio Int  ->  [Ratio Int ->  [Ratio Int]) :: Ratio Int  ->  [Ratio Int ->  [Ratio Int])

module List where
  import qualified Maybe
import qualified Prelude

  insert :: Ord a => a  ->  [a ->  [a]
insert e ls insertBy compare e ls

  insertBy :: (a  ->  a  ->  Ordering ->  a  ->  [a ->  [a]
insertBy vx x [] x : []
insertBy cmp x (vy : vzinsertBy0 vy cmp x vz (vy : vz) (cmp x vy)

  
insertBy0 y cmp x ys' ys GT y : insertBy cmp x ys'
insertBy0 y cmp x ys' ys vw x : ys


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule List
  (insert :: Ratio Int  ->  [Ratio Int ->  [Ratio Int])

module List where
  import qualified Maybe
import qualified Prelude

  insert :: Ord a => a  ->  [a ->  [a]
insert e ls insertBy compare e ls

  insertBy :: (a  ->  a  ->  Ordering ->  a  ->  [a ->  [a]
insertBy vx x [] x : []
insertBy cmp x (vy : vzinsertBy0 vy cmp x vz (vy : vz) (cmp x vy)

  
insertBy0 y cmp x ys' ys GT y : insertBy cmp x ys'
insertBy0 y cmp x ys' ys vw x : ys


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(ww41900), Succ(ww42300)) → new_primCmpNat(ww41900, ww42300)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(ww5900), Succ(ww401000)) → new_primPlusNat(ww5900, ww401000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(ww16000), Succ(ww17100)) → new_primMulNat(ww16000, Succ(ww17100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat0(Succ(ww30000), ww40100) → new_primMulNat0(ww30000, ww40100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2600)) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy028(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35700)) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy045(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Zero) → new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy048(ww3000, ww3100, ww41, Succ(ww3410)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35900))) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy022(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy037(ww40100, ww3100, ww41, Succ(ww2800)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy037(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy049(ww4000000, ww40100, ww3100, ww41, Succ(ww3670)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy035(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy046(ww3000, ww3100, ww41, Succ(ww3350)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy038(ww4000000, ww40100, ww3100, ww41, Succ(ww2820)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy033(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
new_insertBy07(ww3000, ww3100, ww41, Succ(ww700)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy014(ww4000000, ww3100, ww41, Succ(ww1260)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy040(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1770)) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy049(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy036(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy014(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy047(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy021(ww4000000, ww3000, ww3100, ww41, Succ(ww1630)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy044(Pos(Zero), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy021(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy043(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy083(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, Succ(ww860)) → new_insertBy083(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Zero) → new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy048(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Zero) → new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy045(ww4000000, ww3000, ww3100, ww41, Succ(ww3310)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy010(ww4000000, ww40100, ww3100, ww41, Succ(ww1020)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy012(ww4000000, ww40100, ww3100, ww41, Succ(ww1080)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy025(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy035(ww3000, ww3100, ww41, Succ(ww2500)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy051(ww4000000, ww40100, ww3100, ww41, Succ(ww3730)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy046(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy016(ww4000000, ww3100, ww41, Succ(ww1320)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35900)) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Zero) → new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy012(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
new_insertBy044(Pos(Zero), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy084(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
new_insertBy028(ww3100, ww41, Succ(ww2150)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy072(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
new_insertBy034(ww4000000, ww3000, ww3100, ww41, Succ(ww2460)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy044(Neg(Zero), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy055(ww4000000, ww3100, ww41, Succ(ww3970)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy086(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy050(ww40100, ww3100, ww41, Succ(ww3710)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy079(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy050(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy043(ww3100, ww41, Succ(ww3100)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy013(ww40100, ww3100, ww41, Succ(ww1120)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy040(ww4000000, ww3100, ww41, Succ(ww3000)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2620)) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy09(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy011(ww40100, ww3100, ww41, Succ(ww1060)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy08(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy032(ww4000000, ww3000, ww3100, ww41, Succ(ww2400)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3530)) → new_insertBy080(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9400))) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy0(Neg(Zero), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy027(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy023(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy052(ww40100, ww3100, ww41, Succ(ww3770)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy044(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
new_insertBy070(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy051(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy042(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy024(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy036(ww4000000, ww40100, ww3100, ww41, Succ(ww2760)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy044(Pos(ww490), ww50, ww51, Neg(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9200)) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
new_insertBy08(ww4000000, ww3000, ww3100, ww41, Succ(ww720)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy06(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy017(ww3100, ww41, Succ(ww1360)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
new_insertBy062(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Zero) → new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
new_insertBy041(ww3100, ww41, Succ(ww3040)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy019(ww4000000, ww3000, ww3100, ww41, Succ(ww1570)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, Succ(ww880)) → new_insertBy084(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy038(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy032(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy053(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy015(ww3100, ww41, Succ(ww1300)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)
new_insertBy033(ww3000, ww3100, ww41, Succ(ww2440)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy030(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy017(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy024(ww40100, ww3100, ww41, Succ(ww1910)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy030(ww3100, ww41, Succ(ww2210)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9200))) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy031(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy026(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Zero) → new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Zero) → new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
new_insertBy078(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy0(Neg(ww240), ww25, ww26, Pos(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3510)) → new_insertBy079(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy016(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy020(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy013(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
new_insertBy053(ww4000000, ww3100, ww41, Succ(ww3910)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy0(Pos(ww240), ww25, ww26, Neg(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy022(ww3000, ww3100, ww41, Succ(ww1670)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy039(ww40100, ww3100, ww41, Succ(ww2860)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy09(ww3000, ww3100, ww41, Succ(ww760)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy080(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Zero) → new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy019(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy042(ww4000000, ww3100, ww41, Succ(ww3060)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy044(Neg(Zero), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35700))) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1790)) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy029(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy015(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy029(ww4000000, ww3100, ww41, Succ(ww2170)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy018(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy011(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy039(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9400)) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
new_insertBy044(Neg(ww490), ww50, ww51, Pos(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy052(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy05(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy07(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy041(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy010(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy0(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat1(new_primMulNat1(ww3000, ww40100), ww40100))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy047(ww4000000, ww3000, ww3100, ww41, Succ(ww3370)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy027(ww4000000, ww3100, ww41, Succ(ww2110)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy056(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy054(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy056(ww3100, ww41, Succ(ww4010)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy0(Neg(Zero), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy064(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
new_insertBy023(ww4000000, ww40100, ww3100, ww41, Succ(ww1870)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
new_insertBy025(ww4000000, ww40100, ww3100, ww41, Succ(ww1930)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy0(Pos(Zero), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy06(ww4000000, ww3000, ww3100, ww41, Succ(ww660)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy026(ww40100, ww3100, ww41, Succ(ww1970)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy034(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy020(ww3000, ww3100, ww41, Succ(ww1610)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy055(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy082(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy0(Pos(Zero), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
new_insertBy054(ww3100, ww41, Succ(ww3950)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)

The set Q consists of the following terms:

new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 6 SCCs.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy025(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy030(ww3100, ww41, Succ(ww2210)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy017(ww3100, ww41, Succ(ww1360)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy025(ww4000000, ww40100, ww3100, ww41, Succ(ww1930)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy026(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy016(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy026(ww40100, ww3100, ww41, Succ(ww1970)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy029(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy013(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy016(ww4000000, ww3100, ww41, Succ(ww1320)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy029(ww4000000, ww3100, ww41, Succ(ww2170)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy012(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy030(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy017(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy013(ww40100, ww3100, ww41, Succ(ww1120)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy012(ww4000000, ww40100, ww3100, ww41, Succ(ww1080)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)

The set Q consists of the following terms:

new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy038(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy039(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy038(ww4000000, ww40100, ww3100, ww41, Succ(ww2820)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy052(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy051(ww4000000, ww40100, ww3100, ww41, Succ(ww3730)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy051(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy042(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy039(ww40100, ww3100, ww41, Succ(ww2860)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy043(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy055(ww4000000, ww3100, ww41, Succ(ww3970)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy056(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy056(ww3100, ww41, Succ(ww4010)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy055(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy052(ww40100, ww3100, ww41, Succ(ww3770)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy043(ww3100, ww41, Succ(ww3100)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy042(ww4000000, ww3100, ww41, Succ(ww3060)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)

The set Q consists of the following terms:

new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, Succ(ww880)) → new_insertBy084(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
new_insertBy084(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1790)) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
new_insertBy086(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy018(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy022(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy09(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9200))) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy08(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9400)) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
new_insertBy05(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy07(ww3000, ww3100, ww41, Succ(ww700)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Zero) → new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Zero) → new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9400))) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1770)) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy07(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy0(Neg(Zero), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
new_insertBy0(Neg(ww240), ww25, ww26, Pos(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy021(ww4000000, ww3000, ww3100, ww41, Succ(ww1630)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy0(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat1(new_primMulNat1(ww3000, ww40100), ww40100))
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy021(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy020(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy083(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
new_insertBy0(Neg(Zero), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy064(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, Succ(ww860)) → new_insertBy083(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy0(Pos(ww240), ww25, ww26, Neg(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9200)) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy08(ww4000000, ww3000, ww3100, ww41, Succ(ww720)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy06(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy022(ww3000, ww3100, ww41, Succ(ww1670)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy0(Pos(Zero), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
new_insertBy06(ww4000000, ww3000, ww3100, ww41, Succ(ww660)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy062(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
new_insertBy09(ww3000, ww3100, ww41, Succ(ww760)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy020(ww3000, ww3100, ww41, Succ(ww1610)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Zero) → new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Zero) → new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy0(Pos(Zero), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
new_insertBy019(ww4000000, ww3000, ww3100, ww41, Succ(ww1570)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy019(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)

The set Q consists of the following terms:

new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy049(ww4000000, ww40100, ww3100, ww41, Succ(ww3670)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy040(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy054(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy050(ww40100, ww3100, ww41, Succ(ww3710)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy041(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy049(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy036(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy041(ww3100, ww41, Succ(ww3040)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy050(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy053(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy053(ww4000000, ww3100, ww41, Succ(ww3910)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy036(ww4000000, ww40100, ww3100, ww41, Succ(ww2760)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy054(ww3100, ww41, Succ(ww3950)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy037(ww40100, ww3100, ww41, Succ(ww2800)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy040(ww4000000, ww3100, ww41, Succ(ww3000)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy037(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)

The set Q consists of the following terms:

new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy024(ww40100, ww3100, ww41, Succ(ww1910)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy011(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy011(ww40100, ww3100, ww41, Succ(ww1060)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy027(ww4000000, ww3100, ww41, Succ(ww2110)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy028(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy028(ww3100, ww41, Succ(ww2150)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy014(ww4000000, ww3100, ww41, Succ(ww1260)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy015(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy024(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy010(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy027(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy014(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy015(ww3100, ww41, Succ(ww1300)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy023(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy010(ww4000000, ww40100, ww3100, ww41, Succ(ww1020)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy023(ww4000000, ww40100, ww3100, ww41, Succ(ww1870)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)

The set Q consists of the following terms:

new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy032(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2600)) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy044(Pos(Zero), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35700))) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
new_insertBy072(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
new_insertBy034(ww4000000, ww3000, ww3100, ww41, Succ(ww2460)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35700)) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
new_insertBy044(Neg(Zero), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy045(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Zero) → new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy079(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
new_insertBy048(ww3000, ww3100, ww41, Succ(ww3410)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35900))) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
new_insertBy033(ww3000, ww3100, ww41, Succ(ww2440)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2620)) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy035(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy044(Neg(ww490), ww50, ww51, Pos(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
new_insertBy046(ww3000, ww3100, ww41, Succ(ww3350)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy032(ww4000000, ww3000, ww3100, ww41, Succ(ww2400)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy033(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3530)) → new_insertBy080(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy031(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy078(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3510)) → new_insertBy079(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy047(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy044(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy044(Pos(Zero), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
new_insertBy047(ww4000000, ww3000, ww3100, ww41, Succ(ww3370)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy070(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Zero) → new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy048(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy045(ww4000000, ww3000, ww3100, ww41, Succ(ww3310)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Zero) → new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy044(Pos(ww490), ww50, ww51, Neg(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
new_insertBy035(ww3000, ww3100, ww41, Succ(ww2500)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy034(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy046(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy080(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
new_insertBy082(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35900)) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Zero) → new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy044(Neg(Zero), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)

The set Q consists of the following terms:

new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: